% !Mode:: "TeX:UTF-8"
\chapter{Доказательства теорем и лемм}\label{sec:proofs}
%\addcontentsline{toc}{chapter}{Приложение А: Таблицы ограничений}

\begin{lemma}\label{QuantorElimination}
Для любых неотрицательных целых чисел $x$, $y$ и $N$ таких, что $0 \leqslant x, y < 2^N$, справедливо следующее (сравнения беззнаковые):
$$( \exists k \in \mathds{N} : x < 2^k \leqslant y ) \Leftrightarrow (y > x ~\wedge~ x \oplus y > x)$$
\end{lemma}
\begin{proof}
В доказательстве будет использована очевидная эквивалентность: $x < 2^k \Leftrightarrow x_{1..N-k} = 0$. Здесь и далее $t_{a..b}$ будет обозначать число, составленное конкатенацией бит $t_a$, $t_{a+1}$, ..., $t_b$.

1) Докажем, что
$$\left\{\begin{array}{lc}
( \exists k \in \mathds{N} : x < 2^k \leqslant y ) \Rightarrow y > x & (1)\\
( \exists k \in \mathds{N} : x < 2^k \leqslant y ) \Rightarrow  x \oplus y > x & (2)\\
\end{array}\right.$$

(1) очевидно.

Докажем (2). $(x \oplus y)_{1..N-k} = x_{1..N-k} \oplus y_{1..N-k} = y_{1..N-k} \neq 0$ (старшие биты $x$ равны нулю, т.к. $x < 2^k$). Значит, $x \oplus y \geqslant 2^k > x$. Доказано.

2) Докажем, что $( \forall k \in \mathds{N} : (x < 2^k \rightarrow y < 2^k )) \Rightarrow (y \leqslant x ~\vee~ x \oplus y \leqslant x)$.

При $x \geqslant y$ следствие импликации тождественно истинно, значит и вся импликация истинна.

Рассмотрим случай $x < y$. Будем доказывать по следующей схеме:

$( \forall k \in \mathds{N} : (x < 2^k \rightarrow y < 2^k )) \Rightarrow\\
\left[\begin{array}{l}
\exists n \in \mathds{N} : x < 2^n \wedge y < 2^n \wedge x \geqslant 2^{n-1} \wedge y \geqslant 2^{n-1}\\
\exists m \in \mathds{N} : y < 2^m \leqslant x\\
\end{array}\right.
\Rightarrow (x \oplus y \leqslant x)$

Неформально говоря, если про $x$ и $y$ нельзя сказать, что у первого больше нулевых старших бит, чем у второго, то либо у них одинаковое количество старших нулевых бит, либо у второго их больше. Докажем это.

Первый шаг. Рассмотрим множество $\{k \in \mathds{N} | x < 2^k\}$. Это множество непустое (поскольку $x < 2^N$), а, значит, обладает нижней гранью. Иными словами, существует $k'$ такое, что $x < 2^{k'}$ и $x \geqslant 2^{k'-1}$. Т.к. $y < x$, то $y < 2^{k'}$. Кроме того, справедлива дизъюнкция: либо $y \geqslant 2^{k'-1}$, либо $y < 2^{k'-1}$. Иными словами, справедлива следующая дизъюнкция:
$$\left[\begin{array}{lc}
\exists (n = k') \in \mathds{N} : x < 2^{k'} \wedge y < 2^{k'} \wedge x \geqslant 2^{k'-1} \wedge y \geqslant 2^{k'-1} & (*)\\
\exists (m = k'{-}1) \in \mathds{N} : y < 2^{k'-1} \leqslant x & (**)\\
\end{array}\right.$$

Второй шаг. Используя первую часть доказательства, из (**) заменой переменных получаем $x \oplus y \leqslant x$. Осталось доказать, что $(\exists n \in \mathds{N} : x < 2^n \wedge y < 2^n \wedge x \geqslant 2^{n-1} \wedge y \geqslant 2^{n-1}) \Rightarrow (x \oplus y \leqslant x)$. Из посылки следует, что $x_{1..N-n+1} = 1$ и $y_{1..N-n+1} = 1$, из чего следует, что $(x \oplus y)_{1..N-n+1} = x_{1..N-n+1} \oplus y_{1..N-n+1} = 1 \oplus 1 = 0$. Значит, $x\oplus y \leqslant x$.
\end{proof}

\theoremtext{\ref{mirror_fullness_none}}{\FullnessMirrorNone}
\begin{proof}
  Особо подчеркну сначала, что в формулировке теоремы $n$ --- количество обращений к таблице в тестовом шаблоне. А в алгоритме построения ограничений $n$ --- количество \textbf{успешных} обращений к таблице в тестовом шаблоне. Чтобы согласовать обозначения, будем далее придерживаться обозначений из алгоритма: ключи в регионах с успешными обращениями обозначать как $k_i$, $R_i$ для $i = 1, 2, ..., n$, а ключа в регионах с неуспешными обращениями обозначать как $k'_j$, $R'_j$ для $j = 1, 2, ..., n'$ ($n$ в формулировке теоремы есть новое $n$ + $n'$).

  Обозначим $L$ --- состояние таблицы перед тестовым шаблоном. Тогда согласно посылке в условии теоремы для каждого допустимого $i$ выполнено: $(k_i || R_i) \in L$ --- и для каждого допустимого $j$ выполнено: $(k'_j || R'_j) \notin L$. Для всех инструкций состояние таблицы одно и то же, поскольку стратегия вытеснения есть \texttt{none} (промах лишь фиксируется, но не <<исправляется>>). Тем самым. $L \supseteq \{ (k_1||R_1), ..., (k_n||R_n) \}$. Отсюда следует, что для каждого допустимого $j$ $(k'_j||R'_j) \notin \{ (k_1||R_1), ..., (k_n||R_n) \}$.

  Кроме того, поскольку $L$ --- состояние таблицы перед тестовым шаблоном, то количество ключей в каждом регионе, которое может находиться в $L$ равно $w$ (по определению $w$). Но поскольку $L \supseteq \{ (k_1||R_1), ..., (k_n||R_n) \}$, то количество различных ключей в каждом регионе в последовательности $(k_i, R_i)$ не может быть больше $w$. Осталось показать, что это количество выражается формулой, представленной в алгоритме. Действительно, для получения количества различных ключей в том же регионе достаточно просматривать все ключи с начала и отсчитывать те из них, что встречаются впервые, т.е. не встречаются среди предыдущих ключей, что и выражено в формуле.

  Итак, если для щаблона в заданном начальном состоянии есть какая-нибудь последовательность ключей в регионах, то система ограничений будет совместна, поскольку на этих же ключах и регионах выполнены ограничения, генерируемые согласно алгоритму.
\end{proof}

\theoremtext{\ref{mirror_fullness}}{\FullnessMirror}
\begin{proof}
Докажем даже более сильное утверждение (из него очевидно будет следовать требуемое в теореме): есть начальное состояние таблицы $L_0$, для него существуют такие $k_1, k_2, ..., k_n$, $R_1, R_2, ..., R_n$, что выполнены все $S_i$ и $P$; спрашивается, будут ли существовать такие $t_1, t_2, ..., t_m$, $r_1, r_2, ..., r_m$, что составленные ограничения (для тех же $k_1, k_2, ..., k_n$, $R_1$, $R_2$, ..., $R_n$) будут выполнены. Весь вопрос в том, как выбрать $t_1, t_2, ..., t_m$, $r_1, r_2, ..., r_m$. Доказательство можно разделить на две части: в первой будет предложен способ выбора $t_1, t_2, ..., t_m$, $r_1, r_2, ..., r_m$, а во второй будет показано, что на них выполняются ограничения.

\paragraph{выбор инициализирующей последовательности} предлагается делать\\следующим образом. Она будет состоять из подпоследовательностей $s_R$ для каждого $R$ из \textbf{множества} $\{R_1, R_2, ..., R_n\}$. Далее рассматривается построение такой подпоследовательности для произвольного $R$. Выберем из $L_0$ ключи, хранящиеся в регионе $R$, ровно в том порядке, в каком они там находятся (речь идет о порядке в смысле перестановок в таблицах вытеснения). Обозначим эту последовательность $V \equiv \langle v_1, v_2, ..., v_q \rangle$. Далее, удалим из последовательности $k_1, k_2, ..., k_n$ те ключи, чьи регионы не равны $R$, и те, которые присутствуют в последовательности $v_1, v_2, ..., v_q$. Обозначим получившуюся последовательность $U \equiv \langle u_1, u_2, ..., u_p\rangle$. Если $p < w$, то выберем $p{-}w$ произвольных ключей, не встречающихся в последовательностях $U$ и $V$. Обозначим эту последовательность $Z$. Тогда $s_R$ будет являться конкатенацией последовательностей $Z$, $U$ и $V$ (именно в этом порядке). Порядок конкатенации последовательностей $s_R$ произвольный. Последовательность $r_1, r_2, ..., r_m$ выбирается в соответствии с выбором последовательности конкатенации $s_R$.

\paragraph{выполнение системы ограничений} По построению все $(t_1||r_1)$, $(t_2||r_2)$, ..., $(t_m||r_m)$ разные. Кроме того, поскольку на $(k_i, R_i)$ выполнены все условия в тестовом шаблоне, то для них выполнено условие количества различных пар (ключ, регион) в каждом регионе для каждой инструкции. Далее, поскольку последовательность $(t_i, r_i)$ оканчивается последовательностью, дублирующей $L_0$ и стратегия вытеснения является существенно вытесняющей, то после таких инициализирующих обращений состояние таблиц станет точно таким же, каким оно было до инициализирующих обращений. Это значит, что для $(k_i, R_i)$ выполнены ограничения <<быть вытесненным>> (они и есть $S_i$). И поскольку последовательность $(t_1, r_1)$, $(t_2, r_2)$, .., $(t_m, r_m)$ содержит все $(k_1, R_1)$, ..., $(k_n, R_n)$, то выполнены ограничения\\$(k_i||R_i) \in \{(t_1||r_1), (t_2||r_2), ..., (t_m||r_m), (k_1||R_1), (k_2||R_2), ..., (k_{i-1}||R_{i-1})\}$.
\end{proof}

\begin{lemma}\label{PseudoLRUNolDisplacing}
Рассматривается последовательность промахов при стратегии вытеснения \PseudoLRU. Тогда в результате $w{-}1$ промаха строка региона на позиции 0 не будет вытеснена.
\end{lemma}
\begin{proof}
    Доказательство для лучшей читабельности приведено для случая $w = 8$, хотя всё аналогичное очевидным образом переносится на случай произвольного $w = 2^W$.

    Последняя строка таблицы вытеснения для \PseudoLRU имеет вид:\\$(m~6~4~5~0~1~2~3)$. Если построить двоичные разложения каждой позиции, то эту же перестановку можно задать следующим образом:
    \begin{itemize}
        \item элемент с позиции $x \in \{\bigl(\begin{smallmatrix}0\\0\\0
\end{smallmatrix}\bigr)_2, \bigl(\begin{smallmatrix}0\\0\\1
\end{smallmatrix}\bigr)_2, \bigl(\begin{smallmatrix}0\\1\\0
\end{smallmatrix}\bigr)_2, \bigl(\begin{smallmatrix}0\\1\\1
\end{smallmatrix}\bigr)_2\}$ перемещается на позицию $x \oplus \bigl(\begin{smallmatrix}1\\0\\0\end{smallmatrix}\bigr)_2$;
        \item элемент с позиции $x \in \{\bigl(\begin{smallmatrix}1\\0\\0
\end{smallmatrix}\bigr)_2, \bigl(\begin{smallmatrix}1\\0\\1
\end{smallmatrix}\bigr)_2\}$ перемещается на позицию $x \oplus \bigl(\begin{smallmatrix}1\\1\\0\end{smallmatrix}\bigr)_2$;
        \item элемент с позиции $x \in \{\bigl(\begin{smallmatrix}1\\1\\0
\end{smallmatrix}\bigr)_2\}$ перемещается на позицию $x \oplus \bigl(\begin{smallmatrix}1\\1\\1\end{smallmatrix}\bigr)_2$;
        \item $m$ помещается на позицию 0.
\end{itemize}

Сокращая обозначения, перефразируем это:
\begin{itemize}
    \item элемент с позиции $x = \bigl(\begin{smallmatrix}0\\X\\X\end{smallmatrix}\bigr)_2$ перемещается на позицию $x \oplus \bigl(\begin{smallmatrix}1\\0\\0 \end{smallmatrix}\bigr)_2$;
    \item элемент с позиции $x = \bigl(\begin{smallmatrix}1\\0\\X\end{smallmatrix}\bigr)_2$ перемещается на позицию $x \oplus \bigl(\begin{smallmatrix}1\\1\\0\end{smallmatrix}\bigr)_2$;
    \item элемент с позиции $x = \bigl(\begin{smallmatrix}1\\1\\0\end{smallmatrix}\bigr)_2$ перемещается на позицию $x \oplus \bigl(\begin{smallmatrix}1\\1\\1\end{smallmatrix}\bigr)_2$;
    \item $m$ помещается на позицию 0.
\end{itemize}

Перевернем каждый столбец. Получится следующий набор правил перемещения в результате промаха:
\begin{itemize}
    \item элемент с позиции $x = \bigl(\begin{smallmatrix}X\\X\\0\end{smallmatrix}\bigr)_2$ перемещается на позицию $x \oplus \bigl(\begin{smallmatrix}0\\0\\1 \end{smallmatrix}\bigr)_2$;
    \item элемент с позиции $x = \bigl(\begin{smallmatrix}X\\0\\1\end{smallmatrix}\bigr)_2$ перемещается на позицию $x \oplus \bigl(\begin{smallmatrix}0\\1\\1\end{smallmatrix}\bigr)_2$;
    \item элемент с позиции $x = \bigl(\begin{smallmatrix}0\\1\\1\end{smallmatrix}\bigr)_2$ перемещается на позицию $x \oplus \bigl(\begin{smallmatrix}1\\1\\1\end{smallmatrix}\bigr)_2$;
    \item $m$ помещается на позицию 0.
\end{itemize}

Под действием этих правил происходят $w{-}1$ перемещений с <<перевернутой>> позиции $\bigl(\begin{smallmatrix}0\\0\\0\end{smallmatrix}\bigr)_2$. Покажем, что это перемещение имеет очень простой вид: 0, 1, 2, ... . Докажем по индукции. База очевидна: позиция изначально равна 0. Индуктивный переход. За позицией $2k$ будет следовать позиция $2k+1$ под действием первого правила. За позицией $2k+1$ будет следовать позиция $2k+2$ под действием остальных правил (0 и последовательность единичных битов инвертируется, что и есть прибавление единицы).

А если перемещение имеет такой вид, то за $w{-}1$ перемещение ни одна из <<перевернутых>> позиций (а, значит, и просто позиций) не равна $w{-}1$ (0, 1, 2, ..., $w{-}2$). А позиция $w{-}1$ --- это и есть позиция вытеснения согласно последней строке таблицы вытеснения для \PseudoLRU.
\end{proof}

\theoremtext{\ref{thm:PseudoLRU_essential}}{\PseudoLRUEssential}
\begin{proof}
    Из леммы~\ref{PseudoLRUNolDisplacing} следует, что первый внесенный в результате промаха $m$ не будет вытеснен после $w{-}1$ промахов. Однако при каждом промахе какие-то элементы вытесняются. Вносимые на каждом промахе $m$ проходят ту же <<траекторию>>, что и первый. Поэтому к ним снова применима лемма~\ref{PseudoLRUNolDisplacing}. Тем самым после $w$ промахов в регионе будет $w$ штук $m$. Но больше, чем $w$, и не может быть, поскольку это количество строк в регионе. Значит, после $w$ промахов весь регион будет состоять лишь из одних $m$.
\end{proof}

\theoremtext{\ref{thm_mirror_lenth_lru}}{\UpperBoundLRUMirror}
\begin{proof}
  Так же, как это было сделано при доказательстве
  теоремы~\ref{mirror_fullness}, разделим все $k_1, k_2, ..., k_n$
  по регионам. Для каждого задействованного региона составим свою
  инициализирующую последовательность (обозначим ее длину $m_i$
  для $i$'го задействованного региона) и сконкатенируем эти
  последовательности для получения искомой инициализирующей последовательности
   для всего тестового шаблона.
  Подпоследовательность последовательности $k_1, k_2, ..., k_n$,
  соответствующая одному региону, обозначим $y_1, y_2, ...,
  y_{n_i}$.

  Докажем, что $$m_i = M_i + w$$ где $M_i$ -- количество
  элементов последовательности $y_1, y_2, ..., y_{n_i}$, которые дают
  промахи при первых обращениях к ним. Тогда для всего тестового
  шаблона $m = \sum\limits_i m_i = \sum\limits_i M_i + \sum\limits_i w =
  M + w \cdot r$, где $r$ -- количество регионов, задействованных в
  $k_1, k_2, ..., k_n$. Очевидно, что $r \leqslant n$, тем самым это
  приводит к искомой оценке $m \leqslant M + n \cdot w$. Осталось
  доказать формулу для $m_i$.

  Укажем способ построения ключей инициализирующей последовательности. Выберем из $y_1, y_2, ..., y_{n_i}$ подпоследовательность,
  состоящую из тех ключей, которые дают промах и встречаются
  впервые. Обозначим их как $\mu \equiv \mu_1, \mu_2, ..., \mu_{MM_i}$. Они будут первыми ключами в   инициализирующей последовательности. Далее выберем из $y_1, y_2, ..., y_{n_i}$
  все ключи, при обращении к которым происходят попадания.
  Обозначим их как $\eta \equiv \eta_1, \eta_2, ..., \eta_{HH_i}$. Если $MM_i > 0$ и $MM_i +
  HH_i < w + 1$, выберем произвольные различные числа-ключи $\nu \equiv \nu_1, \nu_2,
  ..., \nu_{NN_i}$, которые не встречаются в $y_1, y_2, ..., y_{n_i}$. Итак, инициализирующая последовательность (для данного региона!) представляет собой конкатенацию последовательностей $\mu$, $\eta$ и $\nu$ (в этом порядке).

  Покажем, что такая инициализирующая последовательность удовлетворяет системе ограничений. Все ключи из тестового шаблона, при обращении к которым происходят попадания, встречаются в
  этой последовательности. Это следует из того, что первые такие ключи мы поместили явно (в конец последовательности), а дальнейшие ключи не могут встречаться впервые в тестовом шаблоне, в противном случае они были бы вытеснены до того, как должно быть попадание. Очевидно, что эти первые ключи не вытеснены, поскольку они помещены в конец инициализирующей последовательности. Все ключи, при обращении к которыми происходят промахи, тоже встречаются в этой последовательности (мы их туда поместили явно). При этом поскольку от своего промаха они отделены не менее $w+1$ инструкцией с разными ключами, то к моменту промаха они будут вытеснены (из определения существенной вытесняемости \LRU).

  Длина инициализирующей последовательности для шаблона без промахов (при $MM_i$ = 0) равна количеству ключей в $y_1, y_2, ..., y_{n_i}$, при обращении к
  которым происходят попадания. Их не более чем $w$,
  т.к. последовательность из попаданий может задать лишь часть
  или целиком весь регион. При $MM_i > 0$ длина последовательности
  есть сумма из $M_i$ (поскольку туда включаются все ключи $y_1, y_2,
  ..., y_{n_i}$, при обращении к которым происходят промахи) и
  $w$ (поскольку в инициализирующую последовательность добавляются фиктивные ключи и ключи, при обращении к которым происходят попадания). В обоих случах $m_i = M_i + w$.
\end{proof}

\theoremtext{\ref{thm_pseudoLRU_invariant}}{\PseudoLRUInvariant}
\begin{proof}
  Пусть происходит обращение с позицией $j = (j_1~j_2~\dots~j_W)_2$.
  Тогда согласно каноническому определению \PseudoLRU будет
  произведены следующие изменения: $B_{(1)_2} := j_1; B_{(1~j_1)_2} := j_2; \dots B_{(1~j_1~j_2~\dots~j_{W-1})_2} := j_W$. Однако только часть этих изменений повлияет на
  $(\alpha_1~\alpha_2~\dots~\alpha_W)$, $\alpha_1 = B_{(1)_2}^{\neg i_1}, \alpha_2 = B_{(1~i_1)_2}^{\neg i_2}, \dots, \alpha_W = B_{(1~i_1~i_2~\dots~i_{W-1})_2}^{\neg i_W}$. А именно влияние будет на те элементы вектора, у которых совпадают индексы с изменяемыми элементами согласно каноническому определению. Иными словами,
  изменение $B_{(1~j_1~j_2~\dots~j_k)_2}$ будет влиять на
  $B_{(1~i_1~i_2~\dots~i_m)_2}$ тогда и только тогда, когда
  $(1~j_1~j_2~\dots~j_k)_2 = (1~i_1~i_2~\dots~i_m)_2$. Докажем, что при этом $k = m$. Действительно, если $k > m$, то
  $(1~j_1~j_2~\dots~j_k)_2 \geqslant 2^k$, а $(1~i_1~i_2~\dots~i_m)_2 < 2^{m+1} \leqslant 2^k$, что исключает равенство этих чисел.
  Аналогично доказывается невозможность случая $k < m$.

  Условие $(1~j_1~j_2~\dots~j_k)_2 = (1~i_1~i_2~\dots~i_k)_2$
  эквивалентно условию $(j_1~j_2~\dots~j_k)_2$ $\oplus~(i_1~i_2~\dots~i_k)_2 = 0$. Переходя к полным векторам, это условие записывается в виде $(j_1~j_2~\dots~j_W)_2 \oplus
  (i_1~i_2~\dots~i_W)_2 < 2^{W-k+1}$. Или, переходя от векторов к
  числам, $i \oplus j < 2^{W-k+1}$.

  При этом изменение элементов вектора
  ($\alpha_1~\alpha_2~\dots~\alpha_W$) будет происходить следующим  образом (используется определение степени через сложение по модулю 2: $x^y \equiv x \oplus y \oplus 1$): $\alpha_k :=
  (B_{(1~j_1~j_2~\dots~j_{k-1})_2})^{\neg i_k} =
  (B_{(1~j_1~j_2~\dots~j_{k-1})_2}) \oplus (\neg i_k) \oplus 1 =
  B_{(1~j_1~j_2~\dots~j_{k-1})_2} \oplus i_k = j_k \oplus i_k$. Так как $(j_1~j_2~\dots~j_{k-1})_2 = (i_1~i_2~\dots~i_{k-1})_2$, то $(j_1~j_2~\dots~j_{k-2})_2 = (i_1~i_2~\dots~i_{k-2})_2$ и $i_{k-1} = j_{k-1}$. В таком случае изменяется и $\alpha_{k-1}$, причем $\alpha_{k-1} := i_{k-1} \oplus j_{k-1} = 0$. Аналогично
  рассуждая, получим, что $\alpha_{k-2} := 0,~\dots~\alpha_1 := 0$.
  Иными словами, возможно даже вычислить изменения предыдущих
  элементов -- всем им присваивается значение 0. Найдется такой $p$,
  что $i_1 = j_1~\wedge~i_2 = j_2~\wedge~i_{p-1} =
  j_{p-1}~\wedge~i_p \neq j_p$. В этом случае изменяется
  $\alpha_p$ следующим образом: $\alpha_p := i_p \oplus j_p = 1$.
  Или записывая это условие с использованием чисел $i$ и $j$: $2^{W-p} \leqslant i
  \oplus j < 2^{W-p+1}$.

  Таким образом, получаем, что для $i \oplus j \in
  [\frac{w}{2^k},~\frac{w}{2^{k-1}})$ будет произведены следующие
  присваивания: $\alpha_k := 1,~\alpha_{k-1} := 0,~\alpha_{k-2} :=
  0,~\dots~\alpha_1 := 0$, остальные элементы не будут изменены. Для
  $i \oplus j = 0$, т.е. $i = j$ все элементы $\alpha_k := i_k \oplus
  j_k = 0$. Причем изменение определяется только суммой по модулю 2
  чисел $i$ и $j$, что и является относительной позицией $j$
  относительно $i$.

  Осталось разобраться с ветвью вытесняемого ключа. Это будет такая
  позиция $i = (i_1~i_2~\dots~i_W)_2$, для которой справедливы
  уравнения $i_1 = \neg B_{k_1}~\wedge~i_2 = \neg
  B_{k_2}~\wedge~\dots~\wedge~i_W = \neg B_{k_W}$, где $k_1 = (1)_2$,
  $k_2 = (1~\neg B_{k_1})_2$, ..., $k_W = (1~\neg B_{k_1}~\neg
  B_{k_2}~\dots\\\neg B_{k_{W-1}})_2$. Используя уравнения для
  элементов $i$, можно переписать уравнения для элементов $k$
  следующим образом: $k_1 = (1)_2$,
  $k_2 = (1~i_1)_2$, ..., $k_W = (1~i_1~i_2~\dots~i_{W-1})_2$. Таким
  образом, элементы ветви вытесняемого ключа будут вычисляться
  следующим образом: $\alpha_m \equiv B_{(1~i_1~i_2~\dots~i_{m-1})_2}
  \oplus i_m \equiv B_{k_m} \oplus i_m \equiv \neg i_m \oplus i_m
  \equiv 1$. Иными словами, ветвь вытесняемого ключа состоит только
  из единиц.
\end{proof}

\begin{theorem}\label{PLRUusefulThm}
\PLRUusefuls
\end{theorem}
\begin{proof}
  Напомню, что согласно определению на ветвях бинарного дерева строки региона представляются листьями бинарного дерева, а  процесс вытеснения выглядит как <<перекрашивание>> вершин ветвей. Вытесняется та строка, ветвь к которой полностью покрашена в чёрный цвет (такая строка будет сушествовать и будет единственной). На рисунке~\ref{fig:plru_exmp_vytesn} изображен пример процесса перекрашивания для 8-ассоциативной таблицы ($W = \log_2 8 = 3$). В этом примере рассматривается ветвь, ведущая в строку, к которой происходит обращение А. После обращения к своей же строке вся ветвь становится белой: линия из А в В помечена (0 0 0)$^T$. Чем <<глубже>> по оси ординат происходит обращение, тем <<глубже>> становится белой ветвь (значение по оси ординат означает количество подряд вершин ветви, начиная с первой (самой верхней в векторах на рисунке), которые становятся равными нулю, а следующая за ней вершина, если она существует, становится равной единице, остальные вершины не меняются). Обращение В --- самое <<мелкое>>, оно лишь меняет первую вершину ветви, делая ее чёрной. Следующее обращение, С, перекрашивает 2 вершины в белый цвет (в том числе и ту вершину, которую только что обращение В покрасило в чёрный цвет) и 1 вершину в чёрный цвет. И так далее. Обратим внимание на обращения F и H. Вершины, которые они закрашивают в чёрный цвет, сохраняют свой цвет до промаха, в котором будет определяться, вытеснять ли данную строку. Это происходит потому, что все следующие обращения происходят с закрашиванием меньшего числа вершин, чем в F и H. В результате обращений A-H на момент промаха I ветвь содержит 2 черные и 1 белую вершину. Значит, соответствующая строка останется в регионе и не будет вытеснена.

  Схема доказательства будет следующей:
  \begin{enumerate}
    \item по определению \PseudoLRU невытеснение происходит в том и только в том случае, когда после последнего обращения к строке к каждому последующему промаху ветвь не покрашена целиком в чёрный цвет:
        \begin{equation}\label{eq:v}
        \mathcal{C}(.....\mathcal{C}(\mathcal{C}( (0~0~...~0)^T, \delta_A), \delta_B), ..., \delta_H) \neq (1~1~...~1)^T
        \end{equation}
        функция $\mathcal{C}$ отображает значение ветви до обращения (* * ... *)$^T$ и <<относительную позицию>> обращения $\delta_*$ в значение ветви после обращения; относительная позиция задает количество белых вершин, перекрашиваемых в рамках обращения;
        функция $\mathcal{C}$ определяется следующим образом ($i = 1, 2, ..., , W, \delta = (\delta_{(1)}~\delta_{(2)}~...~\delta_{(W)})^T, \beta = (\beta_{(1)}~\beta_{(2)}~...~\beta_{(W)})^T, \mathcal{C}(\beta, \delta) = (\gamma_{(1)}~\gamma_{(2)}~...~\gamma_{(W)})^T$), где
        $$\gamma_{(i)} = \begin{cases}\delta_{(i)} , & \text{если $1 \notin \{\delta_{(1)}, \delta_{(2)}, ..., \delta_{(i-1)}\}$}\\ \beta_{(i)}, &\text{иначе}\end{cases} \mbox{~для~}i = 1, 2,..., W$$

    \item первый шаг: выделим специальную подпоследовательность (полезных обращений) из последовательности обращений к региону и покажем, что ее длина меньше $W$ тогда и только тогда, когда выполнено~\ref{eq:v};

    \item второй шаг: покажем, что длина подпоследовательности есть указанная сумма в формулировке теоремы.
  \end{enumerate}

  В примере только в F и H указанная в формулировке теоремы функция полезности равна 1. Для остальных обращений не выполняется как минимум одно из условий в конъюнкции - функции полезности: в А не выполнено первое, в I и последующих не выполнено третье, в В и G не выполнено четвертое условие. Количество обращений, функция полезности которых равна 1, есть 2, что меньше $W$. По теореме в этом случае не должно быть вытеснения -- и это же подтверждает вектор ветви перед промахом I.

  Первый шаг. Фиксируем некоторую строку региона. Фиксируем некоторое обращение I с промахом, расположенное после последнего обращения к этой строке (A) и до обращения, в котором составляются ограничения. Нумерация относительных позиций будет производиться от A и считаться с нуля (относительная позиция в В будет обозначаться $\delta_1$, она же обозначалась $\delta_B$, относительная позиция в C --- $\delta_2$ и т.д.). Обозначим $X \in \{0, 1, ..., 2^W-1\}$ -- ветвь перед I. Составим множество
  $$\begin{array}{c}\mathcal{I} = \{i \in \{1, 2, ..., W\} ~|~ \exists j ~(~ (\delta_j)_{(i)} = 1 ~\wedge~
   1 \notin \{ (\delta_j)_{(1)}, (\delta_j)_{(2)}, ..., (\delta_j)_{(i-1)} \} ~\wedge~\\
   \forall x \in \{0~..~2^W{-}1\}~(  \mathcal{C}(x, \delta_j)_{(i..W)} = \mathcal{C}(\mathcal{C}(x, \delta_j), \delta_{j+1})_{(i..W)} = ... = X_{(i..W)}) ) \}\end{array}$$
   
   $(\delta_j)_{(i)}$ --- это $i$'й элемент вектора $\delta_j$, $X_{(i..W)}$ --- это подвектор вектора $X$, в который вошли биты с $i$'го по $W$'й.

   Поскольку, $\mathcal{I} \subseteq \{1, 2, ..., W\}$, то $|\mathcal{I}| \leqslant W$.

   В рамках шага докажем лемму: $$|\mathcal{I}| < W \Leftrightarrow \mathcal{C}( ...  \mathcal{C}(  \mathcal{C}( (0~0~...~0)^T, \delta_1), \delta_2), ..., \delta_N) \neq (1~1~...~1)^T$$

   Доказательство леммы (докажем противоположный вариант леммы, учитывая, что $|\mathcal{I}| \leqslant W$).

   1) ($\Rightarrow$) ~~ $|\mathcal{I}| = W \Leftrightarrow \forall i \in \{1, 2, ..., W\} ~(~ \exists j ~(~ (\delta_j)_{(i)} = 1 ~\wedge~$ \\ $1 \notin \{ (\delta_j)_{(1)}, (\delta_j)_{(2)}, ..., (\delta_j)_{(i-1)} \} ~\wedge~
   \forall x \in \{0~..~2^W{-}1\}~(  \mathcal{C}(x, \delta_j)_{(i..W)} =$\\
    $\mathcal{C}(\mathcal{C}(x, \delta_j), \delta_{j+1})_{(i..W)} = ... = X_{(i..W)}) ) )$. Раз для любого $x$, то в том числе и для $x = \mathcal{C}( ...  \mathcal{C}(  \mathcal{C}( (0~0~...~0)^T, \delta_1), \delta_2), ..., \delta_{j-1})$. Значит, $\mathcal{C}(x, \delta_j)_{(i)} = (\delta_j)_{(i)} = 1$, значит, и $X_{(i)} = 1$, а поскольку это справедливо для любого $i$, то $X = (1~1~...~1)^T$.

   2) ($\Leftarrow$) ~~  От противного. Допустим, есть такой $i \in \{1..W\}$, который не попал в $\mathcal{I}$, хотя и $X = (1~1~...~1)^T$. Если существует $i' > i$ такой, что $i' \in \mathcal{I}$, то $\mathcal{C}(x, \delta_{j(i')})_{(i'..W)} = ... = X_{(i'..W)}$, но тогда и  $\mathcal{C}(x, \delta_{j(i')})_{(i..W)} = ... = X_{(i..W)} = (0~..0~1~...)^T$ (потому что $i$'ю вершину ветви не красят в чёрный цвет по противному предположению), следовательно, $X_{(i)} = 0$, что противоречит тому, что $X = (1~1~...~1)^T$. Если же такой $i'$ не существует, то $X_{(i)} = \mathcal{C}(x', \delta_0)_{(i)} = (0 0 ... 0)^T = 0$ (поскольку от А до I $i$'ю вершину не красят в чёрный цвет), что опять приводит к противоречию.

   Лемма доказана. А с нею и завершен первый шаг.

   Второй шаг. Покажем, что $|\mathcal{I}| = \sum_{i=1}^{m+n} [u(s_i)]$. Сначала покажем, что $|\mathcal{I}| = |\{ j ~|~ \forall j' {>} j ~ P(\delta_j, \delta_{j'}) \}|$, а далее, поскольку такие $j$ единственны, то $|\mathcal{I}| =$\\ $\sum_j [\forall j' {>} j ~ P(\delta_j, \delta_{j'})]) =  \sum_{i=1}^{m+n} [u(s_i)]$. В действительности форма $u(s_i)$ более сложная, нежели $P$ под квантором всеобщности, но остальные составляющие $u(s_i)$ уже учтены в том, как выбрана область тестового шаблона от обращения А до обращения I.

   Из определения $\mathcal{C}$ следует, что эквивалентной будет следующая форма $\mathcal{I}$: $\mathcal{I} = \{i ~|~ \exists j : i(\delta_j) = i ~\wedge~ \forall j' > j ( i(\delta_j) \geqslant i(\delta_{j'}) ) \}$, где функция $i$ отображает относительную позицию в число вершин ветви, которых обращение по этой позиции красит в белый цвет до первой вершины, которую это обращение красит в чёрный. По теореме о верхней грани непустого множества для каждого $i$, входящего в $\mathcal{I}$, существует единственный максимальный $j$, равный $i(\delta_j)$. Тем самым, $|\mathcal{I}| = |\{j | \forall j' > j ( i(\delta_j) > i(\delta_{j'}) ) \}| = |\{ j ~|~ \forall j' {>} j ~ P(\delta_j, \delta_{j'}) \}|$. Требуемое во втором шаге показано. А с ним завершено и доказательство теоремы.
\end{proof} 